Nuprl Lemma : constant_function_wf
11,40
postcript
pdf
A
,
B
:Type,
f
:(
A
B
). constant_function(
f
;
A
;
B
)
prop{i:l}
latex
Definitions
constant_function(
f
;
A
;
B
)
,
x
:
A
.
B
(
x
)
,
prop{i:l}
,
s
=
t
,
f
(
a
)
,
x
:
A
B
(
x
)
,
t
T
,
Type
origin
A,B:Type, f:(A
B). constant_function(f; A; B) 
prop{i:l} A,B:Type, f:(AB). constant_function(f; A; B) prop{i:l} x:A. B(x)B(x) T